fpf{-}empty $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$<$[], $\lambda$$x$.$\cdot>$